﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace PAT.PN.Utility.Example
{
    class SharedComputerSystem
    {
        /// <summary>
        /// This example is based on example 8.5.10 in http://condor.depaul.edu/rjohnson/dm6th/petri.pdf
        /// </summary>
        /// <returns></returns>
        internal static string SharedComputerSystemProblem()
        {
            StringBuilder sb = new StringBuilder();
            sb.AppendLine("<PN>");
            sb.AppendLine("  <Declaration>");//@@Abcxyz@@");
            sb.AppendLine("  ComNetwork = M1();");
            sb.AppendLine();
            sb.AppendLine("#assert  ComNetwork deadlockfree;");
            sb.AppendLine("#assert  ComNetwork |= &lt;&gt; (process_1 || process_2);");
            sb.AppendLine("#assert  ComNetwork |= ! [] (process_1 || process_2);");
            sb.AppendLine("#assert  ComNetwork |= []&lt;&gt; release_1;");
            sb.AppendLine("#assert  ComNetwork |= []&lt;&gt; (release_1 || release_2);");
            sb.AppendLine("  </Declaration>");
            sb.AppendLine("  <Models>");
            sb.AppendLine("    <Model Name=\"M1\" Parameter=\"\" Zoom=\"1\" PlaceCounter=\"7\" TransitionCounter=\"8\">");
            sb.AppendLine("      <Places>");
            sb.AppendLine("        <Place Name=\"D_available\" NumOfToken=\"1\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"5.4\" Y=\"0.6\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.1\" Y=\"0.4\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"ready_1D\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"4.5\" Y=\"2.3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.7\" Y=\"2.4\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"ready_1P\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"4.5\" Y=\"3.7\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.6\" Y=\"3.5\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"ready_2P\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"6.3\" Y=\"3.6\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.6\" Y=\"3.5\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"ready_2D\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"6.3\" Y=\"2.2\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.7\" Y=\"2.4\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"finished_2\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"7.9\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"7.6\" Y=\"2.8\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"finished_1\" NumOfToken=\"0\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"2.7\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"2.5\" Y=\"2.8\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("        <Place Name=\"P_available\" NumOfToken=\"1\" Capacity=\"0\">");
            sb.AppendLine("          <Position X=\"5.4\" Y=\"4.9\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.2\" Y=\"5.1\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("        </Place>");
            sb.AppendLine("      </Places>");
            sb.AppendLine("      <Transitions>");
            sb.AppendLine("        <Transition Name=\"process_1\">");
            sb.AppendLine("          <Position X=\"4\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.3\" Y=\"3.1\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"request_1D\">");
            sb.AppendLine("          <Position X=\"4.9\" Y=\"1.5\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.3\" Y=\"1.7\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"request_1P\">");
            sb.AppendLine("          <Position X=\"5\" Y=\"4.3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.8\" Y=\"4.1\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"request_2P\">");
            sb.AppendLine("          <Position X=\"5.8\" Y=\"4.3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.8\" Y=\"4.1\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"process_2\">");
            sb.AppendLine("          <Position X=\"6.8\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"6.1\" Y=\"3\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"request_2D\">");
            sb.AppendLine("          <Position X=\"5.8\" Y=\"1.5\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.8\" Y=\"1.7\" Width=\"0.8\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"release_2\">");
            sb.AppendLine("          <Position X=\"9.2\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"9\" Y=\"2.7\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("        <Transition Name=\"release_1\">");
            sb.AppendLine("          <Position X=\"1.6\" Y=\"3\" Width=\"0.2\" />");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"1\" Y=\"2.7\" Width=\"0.7\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("          <Guard>");
            sb.AppendLine("          </Guard>");
            sb.AppendLine("          <Program>");
            sb.AppendLine("          </Program>");
            sb.AppendLine("        </Transition>");
            sb.AppendLine("      </Transitions>");
            sb.AppendLine("      <Arcs>");
            sb.AppendLine("        <Arc From=\"D_available\" To=\"request_1D\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.135\" Y=\"1.045\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"request_1D\" To=\"ready_1D\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.6\" Y=\"1.9\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"ready_1D\" To=\"process_1\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.1\" Y=\"2.6\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"process_1\" To=\"finished_1\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"3.3\" Y=\"3.2\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"finished_1\" To=\"release_1\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"2.2\" Y=\"2.9\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"release_1\" To=\"D_available\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"3.15\" Y=\"1.9\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"P_available\" To=\"request_1P\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.2\" Y=\"4.645\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"request_1P\" To=\"ready_1P\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.7\" Y=\"4.1\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"ready_1P\" To=\"process_1\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"4.2\" Y=\"3.5\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"release_1\" To=\"P_available\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"3.15\" Y=\"3.86\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"P_available\" To=\"request_2P\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.7\" Y=\"4.7\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"request_2P\" To=\"ready_2P\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"6.2\" Y=\"4\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"ready_2P\" To=\"process_2\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"6.8\" Y=\"3.4\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"process_2\" To=\"finished_2\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"7.3\" Y=\"2.9\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"finished_2\" To=\"release_2\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"8.5\" Y=\"2.9\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"release_2\" To=\"P_available\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"8\" Y=\"4.1\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"D_available\" To=\"request_2D\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"5.8\" Y=\"1\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"request_2D\" To=\"ready_2D\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"6.2\" Y=\"1.8\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"ready_2D\" To=\"process_2\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"6.7\" Y=\"2.6\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("        <Arc From=\"release_2\" To=\"D_available\" Weight=\"1\">");
            sb.AppendLine("          <Label>");
            sb.AppendLine("            <Position X=\"8\" Y=\"1.76\" Width=\"0.25\" />");
            sb.AppendLine("          </Label>");
            sb.AppendLine("        </Arc>");
            sb.AppendLine("      </Arcs>");
            sb.AppendLine("    </Model>");
            sb.AppendLine("  </Models>");
            sb.AppendLine("</PN>");
            return sb.ToString();
        }
    }
}
